COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	FETCH INTEGE.AX
C00004 ENDMK
C⊗;
FETCH INTEGE.AX;
∧I INDUCTION[P←λN.¬(N≥SUCC N)];
∀E PEANO1 0;
∀E GREATER2 SUCC 0;
∀E GREATER3 SUCC N SUCC SUCC N;
∀E PEANO2 N;
∀E PEANO2 SUCC N;
SUBSTR 5 IN 4;
SUBSTR 6 IN 7;
TAUT 1:#1#2#1 8;
∀I 9 N;
TAUT 1:#2 1 2 3 10;
LABEL LEMMA1 = 11;


DECLARE PREDPAR Q(NATNUM,NATNUM);
∧I INDUCTION[P←λN.(¬Q(N,0)∨Q(0,M*N)∨¬∀I K.(¬I=0 ∧ Q(I,K) ⊃ Q(PRED I,K+M)))];
∀E TIMES1 M;
TAUTEQ 12:#1#2⊃12:#2 12 13;
ASSUME ∀N.((Q(N,0)∧∀I K.((¬(I=0)∧Q(I,K))⊃Q(PRED I,K+M)))⊃Q(0,M*N));
∀E 15 SUCC N;
TAUT 14:#1#1 16;
∀I 17 N;
⊃I 15 18;
TAUT 15:⊃14:#2 14 19;
ASSUME 20:#1#1#1;
TAUT 21:#1 21;
TAUT 21:#2 21;
∧I INDUCTION[P←λN1.(N≥N1 ⊃ Q(N-N1,M*N1))];
∀E MINUS2 N;
∀E TIMES1 M;
TAUTEQ 24:#1#2⊃24:#2 22 24 25 26;
ASSUME 27:#1#1#1;
∀E 23 N-N1 M*N1;
ASSUME N≥SUCC N1;